\begin{tabbing}
agree\_on\_common($T$;${\it as}$;${\it bs}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Ca\=se of ${\it as}$\+
\\[0ex]nil $\rightarrow$ True
\\[0ex]$a$.${\it as'}$, rec: $\rightarrow$ Ca\=se of ${\it bs}$\+
\\[0ex]nil $\rightarrow$ True
\\[0ex]$b$.${\it bs'}$, rec: $\rightarrow$ \=$\neg$($a$ $\in$ ${\it bs}$ $\in$ $T$) \& agree\_on\_common($T$;${\it as'}$;${\it bs}$)\+
\\[0ex]$\vee$ $\neg$($b$ $\in$ ${\it as}$ $\in$ $T$) \& agree\_on\_common($T$;${\it as}$;${\it bs'}$)
\\[0ex]$\vee$ $a$ $=$ $b$ $\in$ $T$ \& agree\_on\_common($T$;${\it as'}$;${\it bs'}$)
\-\-\-\\[0ex]\emph{(recursive)}
\end{tabbing}